Termination Proof Script

Consider the TRS R consisting of the rewrite rules

There are 8 dependency pairs:

The approximated dependency graph contains one SCC: {11-14,16,18}.

Consider the SCC {11-14,16,18}. By taking the AF π with π(activate) = π(ACTIVATE) = π(from) = π(n__from) = π(n__s) = π(s) = 1 and π(cons) = π(FIRST) = 2 together with the lexicographic path order with precedence 0 ≻ nil and n__first ≈ first, the rules in {2-11,16,18} are weakly decreasing and the rules in {1,12-14} are strictly decreasing. There is one new SCC.
- Consider the SCC {16,18}. There are no usable rules. By taking the AF π with π(ACTIVATE) = π(n__from) = 1 together with the lexicographic path order with empty precedence, rule 16 is weakly decreasing and rule 18 is strictly decreasing. There is one new SCC.
  - Consider the SCC {16}. By taking the AF π with π(ACTIVATE) = 1 together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (1.73 seconds) --- May 4, 2006